\documentclass[a4paper]{scrartcl}

\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{color}

\hyphenation{Web-Assembly}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\title{Wasm Formal Semantics}

\begin{document}

\small

\maketitle


\subsection*{Syntax}

##{definition: size}

##{syntax+:
  limits
  {globaltype
  tabletype
  memtype}
  {}
  externtype
}

##{syntax: {instr/block}}

##{syntax: {instr/num instr/local instr/global instr/memory} expr}


\subsection*{Typing #{relation: Instr_ok}}

An instruction sequence #{:instr*} is well-typed with an instruction type #{: t_1* -> t_2*}, written #{:instr*} $:$ #{: t_1* -> t_2*}, according to the following rules:

##{rule:
  {Instrs_ok/empty Instrs_ok/seq}
  {Instrs_ok/frame}
}

##{rule+: Instrs_ok/*m* {Instrs_ok/*m*}}

##{rule: {Instr_ok/unreachable Instr_ok/nop Instr_ok/drop}}

##{rule+: Instr_ok/block}

##{rule+: Instr_ok/loop}

##{rule+: Instr_ok/if}


##{rule-ignore: Instr_ok/memory.grow}


\subsection*{Runtime}

##{definition: default_}

##{definition: {funcinst} {func table}}


\subsection*{Reduction #{relation: Step_pure}}

The relation #{Step: config ~> config} checks that a function type is well-formed.

##{rule: Step/pure Step/read}

##{rule+: {Step_read/block Step_read/loop} {Step_pure/if-*}}

##{rule+: Step_pure/if-*}

\end{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
